\begin{tabbing}
$\forall$\=${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $k$:Knd, $x$:Id, $n$:$\mathbb{N}$,\+
\\[0ex]$f$:(decl{-}state(${\it ds}$)$\rightarrow$ma{-}valtype(${\it da}$; $k$)$\rightarrow$fpf{-}cap(${\it ds}$; id{-}deq; $x$; void)).
\-\\[0ex]update{-}spec1($k$; $x$; $n$; $s$,$v$.$f$($s$,$v$)) $\in$ update{-}spec(${\it ds}$; ${\it da}$)
\end{tabbing}